Linear Temporal Logic (LTL) is a mathematical specification logic which is able to capture temporal relationships. It originally results from the field of model checking and verification.